Nuprl Lemma : void-list-equality3
11,40
postcript
pdf
x
,
y
:(Void List). (
x
=
y
)
{(
null(
x
)) & (
null(
y
))}
latex
Definitions
t
T
,
True
,
P
&
Q
,
{
T
}
,
Void
,
type
List
,
[]
,
s
=
t
,
,
x
:
A
B
(
x
)
,
P
Q
,
b
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
origin
x, y:(Void List). (x = y) 
{(
null(x)) & (null(y))} x, y:(Void List). (x = y) {(null(x)) & (null(y))} 
T
B(x) Qb
B(x)x:A. B(x)